Nuprl Lemma : set_leq_wf 13,42

p:PosetSig, ab:|p|. (a  b  
latex


Upsets 1
Definitions of Statementa  b
Definitionsx f y, a  b, , t  T, x:AB(x)
Lemmasposet sig wf, set car wf, set le wf, assert wf

origin